FDL - Nuprl Lemma : links2Fifo-impl_wf

Nuprl Lemma : links2Fifo-impl_wf

es:ES, l1, l2:IdLnk, tg:Id, A:Type.
links2Fifo-impl(es;l1;l2;A;tg)

(A:Type

(B:Type

C:Type

S:(C

C

E

)

R:(C

E

)

(:(C

A

B

)

Top)))

Definitions x. t(x), A c B, P & Q, P Q, links2Fifo-impl(es;l1;l2;A;tg), , t T, x:A. B(x), {T}, P Q, x(s)

Lemmas es-kind-rcv, event system wf, IdLnk wf, Id wf, es-sender wf, rcv wf, es-kind wf, Knd wf, es-loc wf, existse-at wf